Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); |
2 | |
3 | extern int __VERIFIER_nondet_int(); |
4 | /* Generated by CIL v. 1.3.6 */ |
5 | /* print_CIL_Input is true */ |
6 | |
7 | void error(void) |
8 | { |
9 | |
10 | { |
11 | ERROR: __VERIFIER_error(); |
12 | return; |
13 | } |
14 | } |
15 | int m_pc = 0; |
16 | int t1_pc = 0; |
17 | int t2_pc = 0; |
18 | int t3_pc = 0; |
19 | int t4_pc = 0; |
20 | int t5_pc = 0; |
21 | int t6_pc = 0; |
22 | int m_st ; |
23 | int t1_st ; |
24 | int t2_st ; |
25 | int t3_st ; |
26 | int t4_st ; |
27 | int t5_st ; |
28 | int t6_st ; |
29 | int m_i ; |
30 | int t1_i ; |
31 | int t2_i ; |
32 | int t3_i ; |
33 | int t4_i ; |
34 | int t5_i ; |
35 | int t6_i ; |
36 | int M_E = 2; |
37 | int T1_E = 2; |
38 | int T2_E = 2; |
39 | int T3_E = 2; |
40 | int T4_E = 2; |
41 | int T5_E = 2; |
42 | int T6_E = 2; |
43 | int E_1 = 2; |
44 | int E_2 = 2; |
45 | int E_3 = 2; |
46 | int E_4 = 2; |
47 | int E_5 = 2; |
48 | int E_6 = 2; |
49 | int is_master_triggered(void) ; |
50 | int is_transmit1_triggered(void) ; |
51 | int is_transmit2_triggered(void) ; |
52 | int is_transmit3_triggered(void) ; |
53 | int is_transmit4_triggered(void) ; |
54 | int is_transmit5_triggered(void) ; |
55 | int is_transmit6_triggered(void) ; |
56 | void immediate_notify(void) ; |
57 | void master(void) |
58 | { |
59 | |
60 | { |
61 | if (m_pc == 0) { |
62 | goto M_ENTRY; |
63 | } else { |
64 | if (m_pc == 1) { |
65 | goto M_WAIT; |
66 | } else { |
67 | |
68 | } |
69 | } |
70 | M_ENTRY: ; |
71 | { |
72 | while (1) { |
73 | while_0_continue: /* CIL Label */ ; |
74 | { |
75 | E_1 = 1; |
76 | immediate_notify(); |
77 | E_1 = 2; |
78 | } |
79 | { |
80 | while (1) { |
81 | while_1_continue: /* CIL Label */ ; |
82 | m_pc = 1; |
83 | m_st = 2; |
84 | |
85 | goto return_label; |
86 | M_WAIT: ; |
87 | } |
88 | while_1_break: /* CIL Label */ ; |
89 | } |
90 | } |
91 | while_0_break: /* CIL Label */ ; |
92 | } |
93 | |
94 | return_label: /* CIL Label */ |
95 | return; |
96 | } |
97 | } |
98 | void transmit1(void) |
99 | { |
100 | |
101 | { |
102 | if (t1_pc == 0) { |
103 | goto T1_ENTRY; |
104 | } else { |
105 | if (t1_pc == 1) { |
106 | goto T1_WAIT; |
107 | } else { |
108 | |
109 | } |
110 | } |
111 | T1_ENTRY: ; |
112 | { |
113 | while (1) { |
114 | while_2_continue: /* CIL Label */ ; |
115 | t1_pc = 1; |
116 | t1_st = 2; |
117 | |
118 | goto return_label; |
119 | T1_WAIT: |
120 | { |
121 | E_2 = 1; |
122 | immediate_notify(); |
123 | E_2 = 2; |
124 | } |
125 | } |
126 | while_2_break: /* CIL Label */ ; |
127 | } |
128 | |
129 | return_label: /* CIL Label */ |
130 | return; |
131 | } |
132 | } |
133 | void transmit2(void) |
134 | { |
135 | |
136 | { |
137 | if (t2_pc == 0) { |
138 | goto T2_ENTRY; |
139 | } else { |
140 | if (t2_pc == 1) { |
141 | goto T2_WAIT; |
142 | } else { |
143 | |
144 | } |
145 | } |
146 | T2_ENTRY: ; |
147 | { |
148 | while (1) { |
149 | while_3_continue: /* CIL Label */ ; |
150 | t2_pc = 1; |
151 | t2_st = 2; |
152 | |
153 | goto return_label; |
154 | T2_WAIT: |
155 | { |
156 | E_3 = 1; |
157 | immediate_notify(); |
158 | E_3 = 2; |
159 | } |
160 | } |
161 | while_3_break: /* CIL Label */ ; |
162 | } |
163 | |
164 | return_label: /* CIL Label */ |
165 | return; |
166 | } |
167 | } |
168 | void transmit3(void) |
169 | { |
170 | |
171 | { |
172 | if (t3_pc == 0) { |
173 | goto T3_ENTRY; |
174 | } else { |
175 | if (t3_pc == 1) { |
176 | goto T3_WAIT; |
177 | } else { |
178 | |
179 | } |
180 | } |
181 | T3_ENTRY: ; |
182 | { |
183 | while (1) { |
184 | while_4_continue: /* CIL Label */ ; |
185 | t3_pc = 1; |
186 | t3_st = 2; |
187 | |
188 | goto return_label; |
189 | T3_WAIT: |
190 | { |
191 | E_4 = 1; |
192 | immediate_notify(); |
193 | E_4 = 2; |
194 | } |
195 | } |
196 | while_4_break: /* CIL Label */ ; |
197 | } |
198 | |
199 | return_label: /* CIL Label */ |
200 | return; |
201 | } |
202 | } |
203 | void transmit4(void) |
204 | { |
205 | |
206 | { |
207 | if (t4_pc == 0) { |
208 | goto T4_ENTRY; |
209 | } else { |
210 | if (t4_pc == 1) { |
211 | goto T4_WAIT; |
212 | } else { |
213 | |
214 | } |
215 | } |
216 | T4_ENTRY: ; |
217 | { |
218 | while (1) { |
219 | while_5_continue: /* CIL Label */ ; |
220 | t4_pc = 1; |
221 | t4_st = 2; |
222 | |
223 | goto return_label; |
224 | T4_WAIT: |
225 | { |
226 | E_5 = 1; |
227 | immediate_notify(); |
228 | E_5 = 2; |
229 | } |
230 | } |
231 | while_5_break: /* CIL Label */ ; |
232 | } |
233 | |
234 | return_label: /* CIL Label */ |
235 | return; |
236 | } |
237 | } |
238 | void transmit5(void) |
239 | { |
240 | |
241 | { |
242 | if (t5_pc == 0) { |
243 | goto T5_ENTRY; |
244 | } else { |
245 | if (t5_pc == 1) { |
246 | goto T5_WAIT; |
247 | } else { |
248 | |
249 | } |
250 | } |
251 | T5_ENTRY: ; |
252 | { |
253 | while (1) { |
254 | while_6_continue: /* CIL Label */ ; |
255 | t5_pc = 1; |
256 | t5_st = 2; |
257 | |
258 | goto return_label; |
259 | T5_WAIT: |
260 | { |
261 | E_6 = 1; |
262 | immediate_notify(); |
263 | E_6 = 2; |
264 | } |
265 | } |
266 | while_6_break: /* CIL Label */ ; |
267 | } |
268 | |
269 | return_label: /* CIL Label */ |
270 | return; |
271 | } |
272 | } |
273 | void transmit6(void) |
274 | { |
275 | |
276 | { |
277 | if (t6_pc == 0) { |
278 | goto T6_ENTRY; |
279 | } else { |
280 | if (t6_pc == 1) { |
281 | goto T6_WAIT; |
282 | } else { |
283 | |
284 | } |
285 | } |
286 | T6_ENTRY: ; |
287 | { |
288 | while (1) { |
289 | while_7_continue: /* CIL Label */ ; |
290 | t6_pc = 1; |
291 | t6_st = 2; |
292 | |
293 | goto return_label; |
294 | T6_WAIT: |
295 | { |
296 | error(); |
297 | } |
298 | } |
299 | while_7_break: /* CIL Label */ ; |
300 | } |
301 | |
302 | return_label: /* CIL Label */ |
303 | return; |
304 | } |
305 | } |
306 | int is_master_triggered(void) |
307 | { int __retres1 ; |
308 | |
309 | { |
310 | if (m_pc == 1) { |
311 | if (M_E == 1) { |
312 | __retres1 = 1; |
313 | goto return_label; |
314 | } else { |
315 | |
316 | } |
317 | } else { |
318 | |
319 | } |
320 | __retres1 = 0; |
321 | return_label: /* CIL Label */ |
322 | return (__retres1); |
323 | } |
324 | } |
325 | int is_transmit1_triggered(void) |
326 | { int __retres1 ; |
327 | |
328 | { |
329 | if (t1_pc == 1) { |
330 | if (E_1 == 1) { |
331 | __retres1 = 1; |
332 | goto return_label; |
333 | } else { |
334 | |
335 | } |
336 | } else { |
337 | |
338 | } |
339 | __retres1 = 0; |
340 | return_label: /* CIL Label */ |
341 | return (__retres1); |
342 | } |
343 | } |
344 | int is_transmit2_triggered(void) |
345 | { int __retres1 ; |
346 | |
347 | { |
348 | if (t2_pc == 1) { |
349 | if (E_2 == 1) { |
350 | __retres1 = 1; |
351 | goto return_label; |
352 | } else { |
353 | |
354 | } |
355 | } else { |
356 | |
357 | } |
358 | __retres1 = 0; |
359 | return_label: /* CIL Label */ |
360 | return (__retres1); |
361 | } |
362 | } |
363 | int is_transmit3_triggered(void) |
364 | { int __retres1 ; |
365 | |
366 | { |
367 | if (t3_pc == 1) { |
368 | if (E_3 == 1) { |
369 | __retres1 = 1; |
370 | goto return_label; |
371 | } else { |
372 | |
373 | } |
374 | } else { |
375 | |
376 | } |
377 | __retres1 = 0; |
378 | return_label: /* CIL Label */ |
379 | return (__retres1); |
380 | } |
381 | } |
382 | int is_transmit4_triggered(void) |
383 | { int __retres1 ; |
384 | |
385 | { |
386 | if (t4_pc == 1) { |
387 | if (E_4 == 1) { |
388 | __retres1 = 1; |
389 | goto return_label; |
390 | } else { |
391 | |
392 | } |
393 | } else { |
394 | |
395 | } |
396 | __retres1 = 0; |
397 | return_label: /* CIL Label */ |
398 | return (__retres1); |
399 | } |
400 | } |
401 | int is_transmit5_triggered(void) |
402 | { int __retres1 ; |
403 | |
404 | { |
405 | if (t5_pc == 1) { |
406 | if (E_5 == 1) { |
407 | __retres1 = 1; |
408 | goto return_label; |
409 | } else { |
410 | |
411 | } |
412 | } else { |
413 | |
414 | } |
415 | __retres1 = 0; |
416 | return_label: /* CIL Label */ |
417 | return (__retres1); |
418 | } |
419 | } |
420 | int is_transmit6_triggered(void) |
421 | { int __retres1 ; |
422 | |
423 | { |
424 | if (t6_pc == 1) { |
425 | if (E_6 == 1) { |
426 | __retres1 = 1; |
427 | goto return_label; |
428 | } else { |
429 | |
430 | } |
431 | } else { |
432 | |
433 | } |
434 | __retres1 = 0; |
435 | return_label: /* CIL Label */ |
436 | return (__retres1); |
437 | } |
438 | } |
439 | void update_channels(void) |
440 | { |
441 | |
442 | { |
443 | |
444 | return; |
445 | } |
446 | } |
447 | void init_threads(void) |
448 | { |
449 | |
450 | { |
451 | if (m_i == 1) { |
452 | m_st = 0; |
453 | } else { |
454 | m_st = 2; |
455 | } |
456 | if (t1_i == 1) { |
457 | t1_st = 0; |
458 | } else { |
459 | t1_st = 2; |
460 | } |
461 | if (t2_i == 1) { |
462 | t2_st = 0; |
463 | } else { |
464 | t2_st = 2; |
465 | } |
466 | if (t3_i == 1) { |
467 | t3_st = 0; |
468 | } else { |
469 | t3_st = 2; |
470 | } |
471 | if (t4_i == 1) { |
472 | t4_st = 0; |
473 | } else { |
474 | t4_st = 2; |
475 | } |
476 | if (t5_i == 1) { |
477 | t5_st = 0; |
478 | } else { |
479 | t5_st = 2; |
480 | } |
481 | if (t6_i == 1) { |
482 | t6_st = 0; |
483 | } else { |
484 | t6_st = 2; |
485 | } |
486 | |
487 | return; |
488 | } |
489 | } |
490 | int exists_runnable_thread(void) |
491 | { int __retres1 ; |
492 | |
493 | { |
494 | if (m_st == 0) { |
495 | __retres1 = 1; |
496 | goto return_label; |
497 | } else { |
498 | if (t1_st == 0) { |
499 | __retres1 = 1; |
500 | goto return_label; |
501 | } else { |
502 | if (t2_st == 0) { |
503 | __retres1 = 1; |
504 | goto return_label; |
505 | } else { |
506 | if (t3_st == 0) { |
507 | __retres1 = 1; |
508 | goto return_label; |
509 | } else { |
510 | if (t4_st == 0) { |
511 | __retres1 = 1; |
512 | goto return_label; |
513 | } else { |
514 | if (t5_st == 0) { |
515 | __retres1 = 1; |
516 | goto return_label; |
517 | } else { |
518 | if (t6_st == 0) { |
519 | __retres1 = 1; |
520 | goto return_label; |
521 | } else { |
522 | |
523 | } |
524 | } |
525 | } |
526 | } |
527 | } |
528 | } |
529 | } |
530 | __retres1 = 0; |
531 | return_label: /* CIL Label */ |
532 | return (__retres1); |
533 | } |
534 | } |
535 | void eval(void) |
536 | { |
537 | int tmp ; |
538 | |
539 | { |
540 | { |
541 | while (1) { |
542 | while_8_continue: /* CIL Label */ ; |
543 | { |
544 | tmp = exists_runnable_thread(); |
545 | } |
546 | if (tmp) { |
547 | |
548 | } else { |
549 | goto while_8_break; |
550 | } |
551 | if (m_st == 0) { |
552 | int tmp_ndt_1; |
553 | tmp_ndt_1 = __VERIFIER_nondet_int(); |
554 | if (tmp_ndt_1) { |
555 | { |
556 | m_st = 1; |
557 | master(); |
558 | } |
559 | } else { |
560 | |
561 | } |
562 | } else { |
563 | |
564 | } |
565 | if (t1_st == 0) { |
566 | int tmp_ndt_2; |
567 | tmp_ndt_2 = __VERIFIER_nondet_int(); |
568 | if (tmp_ndt_2) { |
569 | { |
570 | t1_st = 1; |
571 | transmit1(); |
572 | } |
573 | } else { |
574 | |
575 | } |
576 | } else { |
577 | |
578 | } |
579 | if (t2_st == 0) { |
580 | int tmp_ndt_3; |
581 | tmp_ndt_3 = __VERIFIER_nondet_int(); |
582 | if (tmp_ndt_3) { |
583 | { |
584 | t2_st = 1; |
585 | transmit2(); |
586 | } |
587 | } else { |
588 | |
589 | } |
590 | } else { |
591 | |
592 | } |
593 | if (t3_st == 0) { |
594 | int tmp_ndt_4; |
595 | tmp_ndt_4 = __VERIFIER_nondet_int(); |
596 | if (tmp_ndt_4) { |
597 | { |
598 | t3_st = 1; |
599 | transmit3(); |
600 | } |
601 | } else { |
602 | |
603 | } |
604 | } else { |
605 | |
606 | } |
607 | if (t4_st == 0) { |
608 | int tmp_ndt_5; |
609 | tmp_ndt_5 = __VERIFIER_nondet_int(); |
610 | if (tmp_ndt_5) { |
611 | { |
612 | t4_st = 1; |
613 | transmit4(); |
614 | } |
615 | } else { |
616 | |
617 | } |
618 | } else { |
619 | |
620 | } |
621 | if (t5_st == 0) { |
622 | int tmp_ndt_6; |
623 | tmp_ndt_6 = __VERIFIER_nondet_int(); |
624 | if (tmp_ndt_6) { |
625 | { |
626 | t5_st = 1; |
627 | transmit5(); |
628 | } |
629 | } else { |
630 | |
631 | } |
632 | } else { |
633 | |
634 | } |
635 | if (t6_st == 0) { |
636 | int tmp_ndt_7; |
637 | tmp_ndt_7 = __VERIFIER_nondet_int(); |
638 | if (tmp_ndt_7) { |
639 | { |
640 | t6_st = 1; |
641 | transmit6(); |
642 | } |
643 | } else { |
644 | |
645 | } |
646 | } else { |
647 | |
648 | } |
649 | } |
650 | while_8_break: /* CIL Label */ ; |
651 | } |
652 | |
653 | return; |
654 | } |
655 | } |
656 | void fire_delta_events(void) |
657 | { |
658 | |
659 | { |
660 | if (M_E == 0) { |
661 | M_E = 1; |
662 | } else { |
663 | |
664 | } |
665 | if (T1_E == 0) { |
666 | T1_E = 1; |
667 | } else { |
668 | |
669 | } |
670 | if (T2_E == 0) { |
671 | T2_E = 1; |
672 | } else { |
673 | |
674 | } |
675 | if (T3_E == 0) { |
676 | T3_E = 1; |
677 | } else { |
678 | |
679 | } |
680 | if (T4_E == 0) { |
681 | T4_E = 1; |
682 | } else { |
683 | |
684 | } |
685 | if (T5_E == 0) { |
686 | T5_E = 1; |
687 | } else { |
688 | |
689 | } |
690 | if (T6_E == 0) { |
691 | T6_E = 1; |
692 | } else { |
693 | |
694 | } |
695 | if (E_1 == 0) { |
696 | E_1 = 1; |
697 | } else { |
698 | |
699 | } |
700 | if (E_2 == 0) { |
701 | E_2 = 1; |
702 | } else { |
703 | |
704 | } |
705 | if (E_3 == 0) { |
706 | E_3 = 1; |
707 | } else { |
708 | |
709 | } |
710 | if (E_4 == 0) { |
711 | E_4 = 1; |
712 | } else { |
713 | |
714 | } |
715 | if (E_5 == 0) { |
716 | E_5 = 1; |
717 | } else { |
718 | |
719 | } |
720 | if (E_6 == 0) { |
721 | E_6 = 1; |
722 | } else { |
723 | |
724 | } |
725 | |
726 | return; |
727 | } |
728 | } |
729 | void reset_delta_events(void) |
730 | { |
731 | |
732 | { |
733 | if (M_E == 1) { |
734 | M_E = 2; |
735 | } else { |
736 | |
737 | } |
738 | if (T1_E == 1) { |
739 | T1_E = 2; |
740 | } else { |
741 | |
742 | } |
743 | if (T2_E == 1) { |
744 | T2_E = 2; |
745 | } else { |
746 | |
747 | } |
748 | if (T3_E == 1) { |
749 | T3_E = 2; |
750 | } else { |
751 | |
752 | } |
753 | if (T4_E == 1) { |
754 | T4_E = 2; |
755 | } else { |
756 | |
757 | } |
758 | if (T5_E == 1) { |
759 | T5_E = 2; |
760 | } else { |
761 | |
762 | } |
763 | if (T6_E == 1) { |
764 | T6_E = 2; |
765 | } else { |
766 | |
767 | } |
768 | if (E_1 == 1) { |
769 | E_1 = 2; |
770 | } else { |
771 | |
772 | } |
773 | if (E_2 == 1) { |
774 | E_2 = 2; |
775 | } else { |
776 | |
777 | } |
778 | if (E_3 == 1) { |
779 | E_3 = 2; |
780 | } else { |
781 | |
782 | } |
783 | if (E_4 == 1) { |
784 | E_4 = 2; |
785 | } else { |
786 | |
787 | } |
788 | if (E_5 == 1) { |
789 | E_5 = 2; |
790 | } else { |
791 | |
792 | } |
793 | if (E_6 == 1) { |
794 | E_6 = 2; |
795 | } else { |
796 | |
797 | } |
798 | |
799 | return; |
800 | } |
801 | } |
802 | void activate_threads(void) |
803 | { int tmp ; |
804 | int tmp___0 ; |
805 | int tmp___1 ; |
806 | int tmp___2 ; |
807 | int tmp___3 ; |
808 | int tmp___4 ; |
809 | int tmp___5 ; |
810 | |
811 | { |
812 | { |
813 | tmp = is_master_triggered(); |
814 | } |
815 | if (tmp) { |
816 | m_st = 0; |
817 | } else { |
818 | |
819 | } |
820 | { |
821 | tmp___0 = is_transmit1_triggered(); |
822 | } |
823 | if (tmp___0) { |
824 | t1_st = 0; |
825 | } else { |
826 | |
827 | } |
828 | { |
829 | tmp___1 = is_transmit2_triggered(); |
830 | } |
831 | if (tmp___1) { |
832 | t2_st = 0; |
833 | } else { |
834 | |
835 | } |
836 | { |
837 | tmp___2 = is_transmit3_triggered(); |
838 | } |
839 | if (tmp___2) { |
840 | t3_st = 0; |
841 | } else { |
842 | |
843 | } |
844 | { |
845 | tmp___3 = is_transmit4_triggered(); |
846 | } |
847 | if (tmp___3) { |
848 | t4_st = 0; |
849 | } else { |
850 | |
851 | } |
852 | { |
853 | tmp___4 = is_transmit5_triggered(); |
854 | } |
855 | if (tmp___4) { |
856 | t5_st = 0; |
857 | } else { |
858 | |
859 | } |
860 | { |
861 | tmp___5 = is_transmit6_triggered(); |
862 | } |
863 | if (tmp___5) { |
864 | t6_st = 0; |
865 | } else { |
866 | |
867 | } |
868 | |
869 | return; |
870 | } |
871 | } |
872 | void immediate_notify(void) |
873 | { |
874 | |
875 | { |
876 | { |
877 | activate_threads(); |
878 | } |
879 | |
880 | return; |
881 | } |
882 | } |
883 | void fire_time_events(void) |
884 | { |
885 | |
886 | { |
887 | M_E = 1; |
888 | |
889 | return; |
890 | } |
891 | } |
892 | void reset_time_events(void) |
893 | { |
894 | |
895 | { |
896 | if (M_E == 1) { |
897 | M_E = 2; |
898 | } else { |
899 | |
900 | } |
901 | if (T1_E == 1) { |
902 | T1_E = 2; |
903 | } else { |
904 | |
905 | } |
906 | if (T2_E == 1) { |
907 | T2_E = 2; |
908 | } else { |
909 | |
910 | } |
911 | if (T3_E == 1) { |
912 | T3_E = 2; |
913 | } else { |
914 | |
915 | } |
916 | if (T4_E == 1) { |
917 | T4_E = 2; |
918 | } else { |
919 | |
920 | } |
921 | if (T5_E == 1) { |
922 | T5_E = 2; |
923 | } else { |
924 | |
925 | } |
926 | if (T6_E == 1) { |
927 | T6_E = 2; |
928 | } else { |
929 | |
930 | } |
931 | if (E_1 == 1) { |
932 | E_1 = 2; |
933 | } else { |
934 | |
935 | } |
936 | if (E_2 == 1) { |
937 | E_2 = 2; |
938 | } else { |
939 | |
940 | } |
941 | if (E_3 == 1) { |
942 | E_3 = 2; |
943 | } else { |
944 | |
945 | } |
946 | if (E_4 == 1) { |
947 | E_4 = 2; |
948 | } else { |
949 | |
950 | } |
951 | if (E_5 == 1) { |
952 | E_5 = 2; |
953 | } else { |
954 | |
955 | } |
956 | if (E_6 == 1) { |
957 | E_6 = 2; |
958 | } else { |
959 | |
960 | } |
961 | |
962 | return; |
963 | } |
964 | } |
965 | void init_model(void) |
966 | { |
967 | |
968 | { |
969 | m_i = 1; |
970 | t1_i = 1; |
971 | t2_i = 1; |
972 | t3_i = 1; |
973 | t4_i = 1; |
974 | t5_i = 1; |
975 | t6_i = 1; |
976 | |
977 | return; |
978 | } |
979 | } |
980 | int stop_simulation(void) |
981 | { int tmp ; |
982 | int __retres2 ; |
983 | |
984 | { |
985 | { |
986 | tmp = exists_runnable_thread(); |
987 | } |
988 | if (tmp) { |
989 | __retres2 = 0; |
990 | goto return_label; |
991 | } else { |
992 | |
993 | } |
994 | __retres2 = 1; |
995 | return_label: /* CIL Label */ |
996 | return (__retres2); |
997 | } |
998 | } |
999 | void start_simulation(void) |
1000 | { int kernel_st ; |
1001 | int tmp ; |
1002 | int tmp___0 ; |
1003 | |
1004 | { |
1005 | { |
1006 | kernel_st = 0; |
1007 | update_channels(); |
1008 | init_threads(); |
1009 | fire_delta_events(); |
1010 | activate_threads(); |
1011 | reset_delta_events(); |
1012 | } |
1013 | { |
1014 | while (1) { |
1015 | while_9_continue: /* CIL Label */ ; |
1016 | { |
1017 | kernel_st = 1; |
1018 | eval(); |
1019 | } |
1020 | { |
1021 | kernel_st = 2; |
1022 | update_channels(); |
1023 | } |
1024 | { |
1025 | kernel_st = 3; |
1026 | fire_delta_events(); |
1027 | activate_threads(); |
1028 | reset_delta_events(); |
1029 | } |
1030 | { |
1031 | tmp = exists_runnable_thread(); |
1032 | } |
1033 | if (tmp == 0) { |
1034 | { |
1035 | kernel_st = 4; |
1036 | fire_time_events(); |
1037 | activate_threads(); |
1038 | reset_time_events(); |
1039 | } |
1040 | } else { |
1041 | |
1042 | } |
1043 | { |
1044 | tmp___0 = stop_simulation(); |
1045 | } |
1046 | if (tmp___0) { |
1047 | goto while_9_break; |
1048 | } else { |
1049 | |
1050 | } |
1051 | } |
1052 | while_9_break: /* CIL Label */ ; |
1053 | } |
1054 | |
1055 | return; |
1056 | } |
1057 | } |
1058 | int main(void) |
1059 | { int __retres1 ; |
1060 | |
1061 | { |
1062 | { |
1063 | init_model(); |
1064 | start_simulation(); |
1065 | } |
1066 | __retres1 = 0; |
1067 | return (__retres1); |
1068 | } |
1069 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2025-08-28 | 17:02:33:080 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2025-08-28 | 17:02:33:155 | INFO | CPAchecker.run | CPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started |
| 2025-08-28 | 17:02:33:173 | INFO | CPAchecker.parse | Parsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/transmitter.06_false-unreach-call_false-termination.cil/transmitter.06_false-unreach-call_false-termination.cil.c" |
| 2025-08-28 | 17:02:34:578 | INFO | CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2025-08-28 | 17:02:34:598 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.arg.lateMerge counterexample.export.exportWitness |
| 2025-08-28 | 17:02:34:598 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2025-08-28 | 17:02:34:612 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ... |
| 2025-08-28 | 17:02:34:684 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration | Using the following resource limits: Thread CPU-time limit of 300s |
| 2025-08-28 | 17:02:35:023 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 17:02:35:476 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 17:02:35:489 | WARNING | CPAs.retrieveCPAOrFail | Warning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA) |
| 2025-08-28 | 17:02:35:493 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ... |
| 2025-08-28 | 17:02:35:500 | INFO | NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'. |
| 2025-08-28 | 17:02:35:529 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 17:02:35:533 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 17:02:35:700 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 17:02:35:767 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 17:02:35:808 | INFO | RestartAlgorithm.run | Starting analysis 1 ... |
| 2025-08-28 | 17:02:35:809 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.run0 | Starting termination algorithm. |
| 2025-08-28 | 17:17:31:709 | WARNING | ForceTerminationOnShutdown$1.shutdownRequested | Shutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination. |
| 2025-08-28 | 17:17:31:721 | WARNING | ShutdownNotifier.shutdownIfNecessary | Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.) |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Restart Algorithm statistics | ||
| Number of algorithms provided | 2 | |
| Number of algorithms used | 1 | |
| Last algorithm used | /cpachecker/config/components/combinations-parallel-termination.properties | |
| Total time for algorithm 1 | 897.107s | |
| PredicateCPA statistics | ||
| Number of abstractions | 26 | 0% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 23 | 88% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 3 | 12% |
| Times precision was empty | 15 | 58% |
| Times precision was {false} | 0 | 0% |
| Times result was cached | 3 | 12% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 8 | 31% |
| Times result was 'false' | 1 | 4% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 6203 | |
| BDD entailment checks | 16 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 465 | |
| Avg ABE block size | 247.42 | sum: 6433, count: 26, min: 0, max: 465 |
| Number of predicates discovered | 28 | |
| Number of abstraction locations | 2 | |
| Max number of predicates per location | 28 | |
| Avg number of predicates per location | 27 | |
| Total predicates per abstraction | 300 | |
| Max number of predicates per abstraction | 28 | |
| Avg number of predicates per abstraction | 37.50 | |
| Number of irrelevant predicates | 3 | 1% |
| Number of preds handled by boolean abs | 216 | 72% |
| Total number of models for allsat | 3110 | |
| Max number of models for allsat | 1426 | |
| Avg number of models for allsat | 388.75 | |
| Time for post operator | 0.880s | |
| Time for path formula creation | 0.862s | |
| Time for strengthen operator | 0.035s | |
| Time for prec operator | 4.781s | |
| Time for abstraction | 4.733s | Max: 2.180s, Count: 26 |
| Boolean abstraction | 4.582s | |
| Solving time | 0.053s | Max: 0.010s |
| Model enumeration time | 4.514s | |
| Time for BDD construction | 0.197s | Max: 0.004s |
| Time for merge operator | 0.092s | |
| Time for coverage checks | 0.009s | |
| Time for BDD entailment checks | 0.006s | |
| Total time for SMT solver (w/o itp) | 4.567s | |
| Number of path formula cache hits | 9659 | 43% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 0.831s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 128040 | |
| Size of BDD node table | 466043 | |
| Size of BDD cache | 46619 | |
| Size of BDD node cleanup queue | 2.09 | sum: 3030, count: 1449, min: 0, max: 1694 |
| Time for BDD node cleanup | 0.000s | |
| Time for BDD garbage collection | 0.000s | in 0 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (NonTerminationLabelAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.088s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 20587, count: 20597, min: 0, max: 1 [0 x 10, 1 x 20587] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (TerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.028s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 20587, count: 20587, min: 1, max: 1 [1 x 20587] |
| Number of states with assumption transitions | 0 | |
| Termination Algorithm statistics | ||
| Total time | 895.911s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 50% |
| Total time for loop analysis | 895.903s | |
| Avg time per loop analysis | 895.903s | |
| Max time per loop analysis | 895.903s | |
| Number of safety analysis runs | 1 | |
| Avg safety analysis run per loop | 1.00 | |
| Max safety analysis run per loop | 1 for loops [N743] | |
| Total time for safety analysis | 7.688s | |
| Avg time per safety analysis run | 7.688s | |
| Max time per safety analysis run | 7.688s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 888.188s | |
| Avg time per iteration | 888.188s | |
| Max time per iteration | 888.188s | |
| Time for lassos construction | 888.188s | |
| Avg time for lasso construction per iteration | 888.188s | |
| Max time for lasso construction per iteration | 888.188s | |
| Time for stem and loop construction | 0.148s | |
| Avg time for stem and loop construction per iteration | 0.148s | |
| Max time for stem and loop construction per iteration | 0.148s | |
| Time for lassos creation | 888.038s | |
| Avg time for lassos creation per iteration | 888.038s | |
| Max time for lassos creation per iteration | 888.038s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Termination Algorithm statistics | ||
| Total time | 895.911s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 1 | 50% |
| Total time for loop analysis | 895.903s | |
| Avg time per loop analysis | 895.903s | |
| Max time per loop analysis | 895.903s | |
| Number of safety analysis runs | 1 | |
| Avg safety analysis run per loop | 1.00 | |
| Max safety analysis run per loop | 1 for loops [N743] | |
| Total time for safety analysis | 7.688s | |
| Avg time per safety analysis run | 7.688s | |
| Max time per safety analysis run | 7.688s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 888.188s | |
| Avg time per iteration | 888.188s | |
| Max time per iteration | 888.188s | |
| Time for lassos construction | 888.188s | |
| Avg time for lasso construction per iteration | 888.188s | |
| Max time for lasso construction per iteration | 888.188s | |
| Time for stem and loop construction | 0.148s | |
| Avg time for stem and loop construction per iteration | 0.148s | |
| Max time for stem and loop construction per iteration | 0.148s | |
| Time for lassos creation | 888.038s | |
| Avg time for lassos creation per iteration | 888.038s | |
| Max time for lassos creation per iteration | 888.038s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 458 | |
| Total lines | 460 | |
| Line coverage | 0.996 | |
| Visited conditions | 212 | |
| Total conditions | 212 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 740 | |
| Number of CFA edges (per node) | 854 | count: 740, min: 0, max: 6, avg: 1.15 |
| Number of relevant variables | 70 | |
| Number of functions | 29 | |
| Number of loops (and loop nodes) | 2 | sum: 98, min: 22, max: 76, avg: 49.00 |
| Size of reached set | 9184 | |
| Number of reached locations | 616 | 83% |
| Avg states per location | 14 | |
| Max states per location | 49 | at node N595 |
| Number of reached functions | 29 | 100% |
| Number of partitions | 616 | |
| Avg size of partitions | 14 | |
| Max size of partitions | 49 | with key N595 |
| Number of target states | 1 | |
| Size of final wait list | 9 | |
| Time for analysis setup | 1.425s | |
| Time for loading CPAs | 0.015s | |
| Time for loading parser | 0.216s | |
| Time for CFA construction | 1.153s | |
| Time for parsing file(s) | 0.302s | |
| Time for AST to CFA | 0.381s | |
| Time for CFA sanity check | 0.094s | |
| Time for post-processing | 0.243s | |
| Time for loop structure | 0.013s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.666s | |
| Time for function pointers resolving | 0.008s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.126s | |
| Time for collecting variables | 0.082s | |
| Time for solving dependencies | 0.003s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.036s | |
| Time for exporting data | 0.005s | |
| Time for Analysis | 897.110s | |
| CPU time for analysis | 947.970s | |
| Total time for CPAchecker | 898.552s | |
| Total CPU time for CPAchecker | 950.420s | |
| Time for statistics | 0.269s | |
| Time for Garbage Collector | 8.176s | in 5024 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 1646MB ( 1570 MiB) max; 704MB ( 672 MiB) avg; 1993MB ( 1900 MiB) peak | |
| Used non-heap memory | 60MB ( 57 MiB) max; 59MB ( 57 MiB) avg; 61MB ( 58 MiB) peak | |
| Used in PS Old Gen pool | 1135MB ( 1082 MiB) max; 571MB ( 545 MiB) avg; 1135MB ( 1082 MiB) peak | |
| Allocated heap memory | 3349MB ( 3194 MiB) max; 1794MB ( 1711 MiB) avg | |
| Allocated non-heap memory | 63MB ( 60 MiB) max; 63MB ( 60 MiB) avg | |
| Total process virtual memory | 14915MB ( 14224 MiB) max; 14896MB ( 14206 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.termination | true |
| 2 | analysis.machineModel | Linux64 |
| 3 | analysis.name | terminationAnalysis |
| 4 | analysis.programNames | Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/transmitter.06_false-unreach-call_false-termination.cil/transmitter.06_false-unreach-call_false-termination.cil.c |
| 5 | analysis.restartAfterUnknown | true |
| 6 | counterexample.export.exportWitness | false |
| 7 | cpa.arg.lateMerge | prevent |
| 8 | language | C |
| 9 | log.level | INFO |
| 10 | parser.usePreprocessor | true |
| 11 | restartAlgorithm.configFiles | components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive |
| 12 | specification | |
| 13 | statistics.print | true |
| 14 | termination.config | terminationAnalysis.properties |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}